Nuprl Lemma : poss-le_wf
11,40
postcript
pdf
poss
:(ES{i}
{i'}),
e1
,
e2
:possible-event{i:l}(
poss
). poss-le{i:l}(
e1
;
e2
)
{i'}
latex
Definitions
True
,
T
,
S
T
,
x
.
t
(
x
)
,
A
c
B
,
e1
e2
,
t
T
,
PossibleEvent(
poss
)
,
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
t
.1
,
E
Lemmas
event
system
wf
,
true
wf
,
squash
wf
,
es-E
wf
,
pi2
wf
,
pi1
wf
,
es-le
wf
origin
poss:(ES{i}
{i'}), e1, e2:possible-event{i:l}(poss). poss-le{i:l}(e1; e2) 
{i'} poss:(ES{i}{i'}), e1, e2:possible-event{i:l}(poss). poss-le{i:l}(e1; e2) {i'} 
T
T
x. t(x)
B
e2 Tx:A. B(x)